package no.uio.ifi.cop.cl;

import java.util.HashSet;
import java.util.Set;

import no.uio.ifi.cop.common.Log;

/**
 * An Axiom holds an argument and its conclusion.
 *
 * Axioms have types which are based on the types
 * of the argument and the conclusion. These will
 * be used in order to apply rules in a fair manner
 * later on, or can be used to for this purpose at
 * least.
 *
 * @version 1.0
 * @author bjarneh@ifi.uio.no
 */

public class Axiom implements Cloneable{

    private static int counter = 0;

    public static final int NOTSET        = 0;
    public static final int GOALRULE      = 1;
    public static final int PLAINRULE     = 2;
    public static final int DISJUNCTRULE  = 3;
    public static final int EXISTRULE     = 4;
    public static final int EXISTDISRULE  = 5;
    public static final int FACTRULE      = 6;

    int type;

    Conjunction lhs;
    RHS rhs;
    
    public Axiom(){
        type = NOTSET;
    }


    public void classify(){
        
        Set<String> lhsSet, rhsSet;
        int lhsType = lhs.getType();
        int rhsType = rhs.getType();
        boolean existRule = false;

        if( lhsType == Formula.CONSTANT ){

            if( rhsType != Formula.CONJUNCTION ){
                StringBuilder sb = new StringBuilder();
                sb.append("\nfact-rule RHS must be: conjunction\n\n");
                sb.append(String.format("%s => %s", lhs, rhs ) );
                Log.fatal(String.format("%s\n", sb));
            }

            this.type = FACTRULE;
            return;
        }

        if( rhsType == Formula.CONSTANT ){

            if( lhsType != Formula.CONJUNCTION ){

                StringBuilder sb = new StringBuilder();
                sb.append("\ngoal-rule must have LHS conjunction\n\n");
                sb.append(String.format("%s => %s", lhs, rhs) );
                Log.fatal(String.format(" %s\n", sb));

            }

            this.type = GOALRULE;
            return;
        }

        // now we know that we have ordinary formulas in both
        // left and right side of implication, time to count variables
        // and check for disjunction in the RHS

        rhsSet = new HashSet<String>();
        lhsSet = new HashSet<String>();

        rhs.gatherVariables( rhsSet );
        lhs.gatherVariables( lhsSet );

        if( ! lhsSet.containsAll( rhsSet ) ){
            existRule = true;
        }

        if( existRule ){

            if( rhsType == Formula.DISJUNCTION ){
                this.type = EXISTDISRULE;
            }else{
                this.type = EXISTRULE;
            }

        }else{

            if( rhsType == Formula.DISJUNCTION ){
                this.type = DISJUNCTRULE;
            }else{
                this.type = PLAINRULE;
            }

        }

    }

    public Conjunction getLHS(){
        return lhs;
    }

    public RHS getRHS(){
        return rhs;
    }

    public int getType(){
        if(type == NOTSET){
            classify();
        }
        return type;
    }

    public void setLHS(Conjunction lhs){
        this.lhs = lhs;
    }

    public void setRHS(RHS rhs){
        this.rhs = rhs;
    }

    public Axiom apply(Substitution subst){
        lhs.apply( subst );
        rhs.apply( subst );
        return this;
    }

    public String strType(){
        switch( getType() ){
            case PLAINRULE      : return "[plain]";
            case GOALRULE       : return "[goal>]";
            case EXISTRULE      : return "[exist]";
            case DISJUNCTRULE   : return "[disju]";
            case EXISTDISRULE   : return "[exdis]";
            case FACTRULE       : return "[fact>]";
            default:              return "[n/a]  ";
        }
    }

    public String toString(){
        return String.format("%s %s => %s .", strType(), lhs, rhs);
    }

    public Axiom clone(){
        Axiom ax2 = new Axiom();
        ax2.setLHS( lhs.clone() );
        ax2.setRHS( rhs.clone() );
        ax2.type = getType();
        return ax2;
    }
}
